#include "predicates.h"
#include "system.h"
#include "tuple.h"

// Free all resources associated to a node
class freeResources : public OnceProver {
predicateName("free.resources")

  bool proveOnce () {
    Node *node = tuple->nodes[1].final ();
    system->globals.mutexMap.erase (node);
    system->globals.streamMap.erase (node);
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<freeResources, Tuple::ID, 2> freeResRegistrar;

class get : public OnceBindTupleProver {
predicateName("get")

  bool proveOnce () {
    Globals &globals = system->globals;
    globals.lock.lockRead ();
    Globals::VarMap::iterator iter = globals.varMap.find (
        tuple->nodes[1].final ());
    pNode *node = iter != globals.varMap.end () ? &iter->second : 0;
    globals.lock.unlockRead ();
    return node && binder.bind (*tuple->nodes[2], **node, system->trail);
  }
};

ProverFactoryRegistrar<get, Tuple::ID, 3> getRegistrar;

class getAll : public Prover {
predicateName("get.all")

  getAll () :
    first (true) {
  }

  bool prove () {
    Globals &globals = system->globals;
    globals.lock.lockRead ();

    if(first) { // First run
      first = false;
      binder.capture (system->trail);
      iterator = globals.varMap.begin ();
    } else
      binder.undo (system->trail);

    bool ret = false;

    // Loops while the prefix matches
    while(!ret && iterator != globals.varMap.end ()) {
      ret = binder.bind (*(*iterator).first, *tuple->nodes[1], system->trail)
          && binder.bind (*(*iterator).second, *tuple->nodes[2], system->trail);
      iterator++;
    }

    globals.lock.unlockRead ();
    return ret;
  }

  bool first;
  Globals::VarMap::iterator iterator;
  Binder binder;
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<getAll, Tuple::ID, 3> getAllRegistrar;

class setCall : public OnceProver {
predicateName("set")

  bool proveOnce () {
    Globals &globals = system->globals;
    pNode rep (tuple->nodes[2].node->replicate ()); // Permanent version
    globals.lock.lockWrite ();
    globals.varMap[tuple->nodes[1].final ()] = rep;
    globals.lock.unlockWrite ();
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<setCall, Tuple::ID, 3> setRegistrar;

class setPointer : public OnceProver {
predicateName("set.pointer")

  bool proveOnce () {
    Globals &globals = system->globals;
    globals.lock.lockWrite ();
    globals.varMap[tuple->nodes[1].final ()] = tuple->nodes[2].node->final ();
    globals.lock.unlockWrite ();
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<setPointer, Tuple::ID, 3> setPointerRegistrar;

class unset : public OnceProver {
predicateName("unset")

  bool proveOnce () {
    Globals &globals = system->globals;
    globals.lock.lockWrite ();
    globals.varMap.erase (tuple->nodes[1].final ());
    globals.lock.unlockWrite ();
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<unset, Tuple::ID, 2> unsetRegistrar;

class synchronized : public OnceBindTupleProver {
predicateName("synchronized")

  bool proveOnce () {
    Globals &globals = system->globals;
    Prover *prover = Prover::create (*tuple->nodes[2], *system);

    globals.lock.lockWrite ();
    Mutex &mutex = globals.mutexMap[tuple->nodes[1].final ()];
    globals.lock.unlockWrite ();
    mutex.lock ();
    bool ret = prover->prove ();
    mutex.unlock ();

    delete prover;
    return ret;
  }
};

ProverFactoryRegistrar<synchronized, Tuple::ID, 3> synchronizedRegistrar;
